package systemfnomabss

/**
   * adapted from parser for untyped lambda calculus by Miles Sabin 
   */

trait AbstractSyntax  extends systemfnomabss.syntax.Binding with systemfnomabss.syntax.BindingSyntax{ self : AbstractSyntax => 

sealed trait Node


type Term = LTerm
type Type = LType

import TypeManDefs.{LTermTypeMan}
implicit def LTerm2Nominal(arg:LTerm):Nominal[LTerm] = new GenNominal[LTerm](arg) {
  override def fresh(a:Name) = arg match 
    { case special:Record => special.fresh(a)
      case _ => super.fresh(a)
    }
  override def swap(a:Name,b:Name) = arg match {
    case special: Record => special.swap(a,b)
    case _ => super.swap(a,b)
  }
  override def supp:List[Name] = arg match {
    case special:Record => special.supp
    case _ => super.supp
  }
}

sealed abstract class LTerm extends Node /*with Nominal[LTerm]*/{

 // def swap(a:Name, b:Name):LTerm 
 // def fresh(a:Name):Boolean
 // def supp:List[Name]
}
sealed abstract class BaseValue extends LTerm with Primitive with PrimitiveNominal[LTerm,BaseValue] {//nominalByProxyUpBound[LTerm,BaseValue]{
  //for typechecker, can also just be defined there
  def baseType: LType
  //for printing
  val name: String
  
  //necessary to make nominal
  //val nomproxy = PrimitiveIsNominalByProxy(this)
  //def subst(sub: Name => Option[LTerm]): AM[LTerm] = AM.result(this)
}


      case class Tru extends BaseValue{
        val name = "true"
        override def baseType = TyBool()
      }
      case class Fls extends BaseValue{
        val name = "false"
        override def baseType = TyBool()
      }
      case class Unit extends BaseValue{
        val name = "unit"
        override def baseType = TyUnit()
      }
      case class Lit(n: int) extends BaseValue{
        val name = n.toString
        override def baseType = TyInt()
      }
      

   
sealed abstract class GenericallyTypeParamNominalLTerm[Self <:LTerm] extends LTerm with GenNominalByProxy[LTerm, Self] {this:Self =>
  //val typeman:TypeMan[Self]
}
      
case class If(cond: LTerm, pos: LTerm, neg: LTerm) extends LTerm /*GenericallyTypeParamNominalLTerm[If]*/{
  //val typeman = IfTypeMan
}

case class Var(n: Name)  extends LTerm /*GenericallyTypeParamNominalLTerm[Var]*/ with RefersByName{
  def getName:Name = n
  //val typeman = VarTypeMan
}

case class App(fun: LTerm, arg: LTerm) extends LTerm /* GenericallyTypeParamNominalLTerm[App]{val typeman = AppTypeMan}*/

case class Lam(ty:LType, abs: \\[LTerm]) extends LTerm /* GenericallyTypeParamNominalLTerm[Lam]{val typeman = LamTypeMan} */

//ackward, TODO: generalized binders like in nameplate paper to create a fitting type of abstraction for this
case class Let(t1: LTerm, abs: \\[LTerm]) extends LTerm /*GenericallyTypeParamNominalLTerm[Let]{val typeman = LetTypeMan} */

case class TLam(abs: \\[LTerm]) extends LTerm /*GenericallyTypeParamNominalLTerm[TLam]{val typeman = TLamTypeMan}*/
  

case class TApp(t:LTerm, ty: LType) extends LTerm/*GenericallyTypeParamNominalLTerm[TApp]{val typeman = TAppTypeMan}*/

case class Pack(ty:LType, t:LTerm, pubty:LType) extends LTerm /*GenericallyTypeParamNominalLTerm[Pack]{val typeman = PackTypeMan}*/

//composition of body should be: tyvar\\Lam(tyvar, termvar\\body)
case class Unpack(impl: LTerm, pubty_pubvar_body: \\[LTerm]) extends LTerm /*GenericallyTypeParamNominalLTerm[Unpack]{val typeman = UnpackTypeMan}*/

case class RecProj(t: LTerm, label: String) extends LTerm {
  def swap(a:Name, b:Name) = RecProj(t swap(a,b), label)
  def fresh(a:Name) = t.fresh(a)
  def supp = t.supp
}
case class Record(fields: List[(String,LTerm)]) extends LTerm with Nominal[Record]{
  override def toString = "{" + fields.foldRight("")({case ((s,t),xs) => s +"="+ t +", "+ xs} )+ "}"
  def fieldsmap[R](f:LTerm=>R):List[(String,R)] =
    fields.map({case (label,fld)=> (label,f(fld))})
  def field(label:String) = {
      val results = fields.filter( {case (fldlabel,fldtype) => label == fldlabel}).map(_ _2)
      if (results.length == 0)throw new TypeExc("no label "+label+" in record")
      if (results.length >1  )throw new TypeExc("multiple labels "+label+" in record")
      results.head
  } 
  
  def swap(a:Name, b:Name) = Record (
      for { (label, content) <- fields}
      yield (label, content.swap(a,b))
      )
  def fresh(a:Name) = fields.map( {case (n,c)=> c.fresh(a)}).forall( _ == true)                 
  def supp =  fields.flatMap( {case (a,b)=>  b.supp})  
  
}














sealed abstract class LType extends /*Nominal[LType] with*/ Node
import TypeManDefs.LTypeTypeMan
implicit def LType2Nominal(arg:LType):Nominal[LType] = new GenNominal[LType](arg) {
  override def fresh(a:Name) = arg match 
    { case special:TyRecord => special.fresh(a)
      case _ => super.fresh(a)
    }
  override def swap(a:Name,b:Name):LType = arg match {
    case special: TyRecord => special.swap(a,b)
    case _ => super.swap(a,b)
  }
  override def supp:List[Name] = arg match {
    case special:TyRecord => special.supp
    case _ => super.supp
  }
}


sealed abstract class BaseType extends LType  with Primitive with PrimitiveNominal[LType, BaseType]{//NominalByProxyUpBound[LType,BaseType]{
  val name: String
  //val nomproxy = PrimitiveIsNominalByProxy(this)
  //def swap(a: Name, b: Name): Self
  //def fresh(a: Name)=true
  //def supp: List[Name]=Nil
  //def swap(a: Name, b: Name) = this
  //def subst(sub: Name => Option[LType]): LType = this
}
case class TyBool() extends BaseType
{ val name="Bool" }
case class TyInt()  extends BaseType
{ val name="Int"  }
case class TyUnit() extends BaseType
{ val name="Unit" }


sealed abstract class GenericallyTypeParamNominalLType[Self <:LType] extends LType with GenNominalByProxy[LType, Self] {this:Self =>
//val typeman:TypeMan[Self]
}

case class TyVar(n: Name) extends LType /*GenericallyTypeParamNominalLType[TyVar] */with RefersByName{
  def getName = n
  //val typeman = TyVarTypeMan
}
case class TyArr(t1: LType, t2: LType) extends LType /*GenericallyTypeParamNominalLType[TyArr]{val typeman = TyArrTypeMan} */
case class TyUniv(abs: \\[LType]) extends LType /*GenericallyTypeParamNominalLType[TyUniv]{val typeman = TyUnivTypeMan}*/
case class TyExist(abs: \\[LType]) extends LType /*GenericallyTypeParamNominalLType[TyExist]{val typeman = TyExistTypeMan}*/

case class TyRecord(fields: List[(String,LType)]) extends LType with Nominal[TyRecord]{
  def map[R](f:LType=>R):List[(String,R)] =
      fields.map({case (label,fld)=> (label,f(fld))})
  def field(label:String) = {
      val results = fields.filter( {case (fldlabel,fldtype) => label == fldlabel}).map(_ _2)
      if (results.length == 0)throw new TypeExc("no label "+label+" in record")
      if (results.length >1  )throw new TypeExc("multiple labels "+label+" in record")
      results.head
  }

  def swap(a:Name, b:Name) = TyRecord (
      for { (label, content) <- fields}
      yield (label, content.swap(a,b))
      )
  def fresh(a:Name) = fields.map( {case (n,c)=> (c.fresh(a))}).forall( _ == true)                 
  def supp =  fields.flatMap( {case (a,b)=> b.supp})

}









val definingenv:AbstractSyntax = this
object TypeManDefs {



import sybrevolutions.forvalues.{TypeMan,PrimitiveTypeMan,ValSpine,Ty,ConstrExt,Apped}


//dispatcher

implicit lazy val LTermTypeMan: TypeMan[LTerm] = new TypeMan[LTerm]{
  def toValSpine(t:LTerm):ValSpine[LTerm] = t match {
  
  //should never call on primitive, will throw error
  case x:BaseValue => new sybrevolutions.forvalues.PrimitiveTypeMan(x.name).toValSpine(x) 
  
  case x:If => IfTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  
  case x:Var => VarTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  case x:App => AppTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  case x:Lam => LamTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  case x:Let => LetTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  
  case x:TLam => TLamTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  case x:TApp => TAppTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  
  case x:Pack => PackTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  case x:Unpack => UnpackTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  
  case x:RecProj => RecProjTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LTerm]]
  
  //case _ => throw new Exception("unmatched lterm in LTermTypeMan: "+t)
  }
}

import sybrevolutions.forvalues_caseclasses_onclassfile._
import sybrevolutions.forvalues.StringMan
import scala.reflect.Manifest

//have to do compilers job: => this should be done in a later stage



lazy val VarTypeMan:TypeMan[Var] = CaseClass1ToValSpineWithEnv[Var,Name](definingenv)(classOf[Var])//(callvarmanifestmanually,NameTypeMan)

/*new TypeMan[Var]{
      def toValSpine(a:Var):ValSpine[Var] = {val constrf = ConstrExt( (na:Name)=>Var(na), new {val n="Var"})
                                             val nwrap = Ty(a.n)
                                             Apped(constrf,nwrap)}
}*/

//implicit lazy val BindsTermTypeMan:TypeMan[Binds[Term]] = new PrimitiveTypeMan[Binds[Term]]("Binds[Term]")
implicit object BindsTermTypeMan extends PrimitiveTypeMan[Binds[Term]]("Binds[Term"){
  
}
lazy val LamTypeMan: TypeMan[Lam]= CaseClass2ToValSpineWithEnv[Lam,LType,Binds[Term]](definingenv)(classOf[Lam])
  /*new TypeMan[Lam] {
      def toValSpine(a:Lam):ValSpine[Lam] = {val constrf = ConstrExt((t:LType)=> (b:Binds[Term])=>Lam(t,b), new {val n="Lam"})
                                             val twrap = Ty(a.ty)
                                             val bwrap = Ty(a.abs)
                                             Apped(Apped( constrf
                                                        ,twrap)
                                                  , bwrap)
      }                                     
}*/
lazy val IfTypeMan:TypeMan[If] = CaseClass3ToValSpineWithEnv[If,LTerm,LTerm,LTerm](definingenv)(classOf[If])
  /*new TypeMan[If]{ 
  def toValSpine(a:If):ValSpine[If] = {val constrf = ConstrExt( (c:LTerm)=>(p:LTerm)=>(n:LTerm)=>If(c,p,n) , new {val n="If"})
                            val cwrap = Ty(a.cond)
                            val pwrap = Ty(a.pos)
                            val nwrap = Ty(a.neg)
                            Apped(Apped(Apped( constrf
                                           , cwrap)
                                      , pwrap)
                                  , nwrap)
}
}*/
lazy val LetTypeMan: TypeMan[Let]= CaseClass2ToValSpineWithEnv[Let,LTerm,Binds[LTerm]](definingenv)(classOf[Let])
  /*new TypeMan[Let] {
      def toValSpine(a:Let):ValSpine[Let] = {val constrf = ConstrExt((t:LTerm)=> (b:Binds[Term])=>Let(t,b), new {val n="Let"})
                                             val twrap = Ty(a.t1)
                                             val bwrap = Ty(a.abs)
                                             Apped(Apped( constrf
                                                        ,twrap)
                                                  , bwrap)
      }                                  
}*/
lazy val TLamTypeMan:TypeMan[TLam] = CaseClass1ToValSpineWithEnv[TLam,Binds[LTerm]](definingenv)( classOf[TLam])
  /*new TypeMan[TLam]{
      def toValSpine(a:TLam):ValSpine[TLam] = {val constrf = ConstrExt( (b:Binds[Term])=>TLam(b), new {val n="TLam"})
                                             val bwrap = Ty(a.abs) //is this dangerous? NO: not looking inside the abs
                                             Apped(constrf,bwrap)}
}*/
lazy val AppTypeMan: TypeMan[App] = CaseClass2ToValSpineWithEnv[App,LTerm,LTerm](definingenv)(classOf[App])
  /*new TypeMan[App] {
      def toValSpine(a:App):ValSpine[App] = { val constrf = ConstrExt( (l:Term)=>(t:Term) => App(l,t), new {val n="App"})
                                              val lwrap = Ty(a.fun)
                                              val twrap = Ty(a.arg)
                                              Apped(Apped(constrf,lwrap),twrap)
  }
  }*/
lazy val TAppTypeMan: TypeMan[TApp] = CaseClass2ToValSpineWithEnv[TApp,LTerm,LType](definingenv)(classOf[TApp])
  /*new TypeMan[TApp] {
      def toValSpine(a:TApp):ValSpine[TApp] = { val constrf = ConstrExt( (l:Term)=>(t:Type) => TApp(l,t), new {val n="TApp"})
                                              val lwrap = Ty(a.t)
                                              val twrap = Ty(a.ty)
                                              Apped(Apped(constrf,lwrap),twrap)
  }
  }*/
lazy val PackTypeMan:TypeMan[Pack] = CaseClass3ToValSpineWithEnv[Pack,LType,LTerm,LType](definingenv)(classOf[Pack])
  /*new TypeMan[Pack]{ 
      def toValSpine(a:Pack):ValSpine[Pack] = {val constrf = ConstrExt( (a:LType)=>(b:LTerm)=>(c:LType)=>Pack(a,b,c) , new {val n="Pack"})
                                val awrap = Ty(a.ty)
                                val bwrap = Ty(a.t)
                                val cwrap = Ty(a.pubty)
                                Apped(Apped(Apped( constrf
                                               , awrap)
                                          , bwrap)
                                      , cwrap)
  }
}*/
lazy val UnpackTypeMan:TypeMan[Unpack] = CaseClass2ToValSpineWithEnv[Unpack,LTerm,Binds[LTerm]](definingenv)(classOf[Unpack])
  /*new TypeMan[Unpack]{ 
      def toValSpine(a:Unpack):ValSpine[Unpack] = {val constrf = ConstrExt( (c:LTerm)=>(n: \\[LTerm])=>Unpack(c,n) , new {val n="Unpack"})
                                val awrap = Ty(a.impl)
                                val bwrap = Ty(a.pubty_pubvar_body)
                                Apped(Apped( constrf
                                               , awrap)
                                          , bwrap)
  }
}*/
lazy val RecProjTypeMan:TypeMan[RecProj] = CaseClass2ToValSpineWithEnv[RecProj,LTerm,String](definingenv)(classOf[RecProj])




/* 
   * TypeMan definitions for types: bottom layer of boilerplate: implicit to make above instances of gennominal easy
   * 
   */
 


//dispatcher
implicit object LTypeTypeMan extends TypeMan[LType] {
//valspine: even though they are the types of our object language, they are representation objects in the meta language
        def toValSpine(t:LType):ValSpine[LType] = t match {
                case x:BaseType => new sybrevolutions.forvalues.PrimitiveTypeMan(x.name).toValSpine(x)
                //eliminate cast by moving it into valspinemethod
                case x:TyVar => TyVarTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LType]]
                case x:TyArr => TyArrTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LType]]
                case x:TyUniv => TyUnivTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LType]]
                case x:TyExist => TyExistTypeMan.toValSpine(x)//.asInstanceOf[ValSpine[LType]]
}}


implicit object BindsTypeTypeMan extends PrimitiveTypeMan[Binds[Type]]("Binds[Type]") {}


lazy val TyVarTypeMan: TypeMan[TyVar] = CaseClass1ToValSpineWithEnv[TyVar,Name](definingenv)(classOf[TyVar])
  /*new UpboundTypeMan[TyVar] {
   def toValSpineBounded[UpTo>: TyVar](a:TyVar):ValSpine[UpTo] = {val constrf = ConstrExt( (a:Name) => TyVar(a).asInstanceOf[UpTo], new {val n="TyVar"})
                                              val awrap = Ty(a.n)
                                              Apped(constrf,awrap)
                                             }
   }*/
lazy val TyArrTypeMan:TypeMan[TyArr] = CaseClass2ToValSpineWithEnv[TyArr,LType,LType](definingenv)(classOf[TyArr])
  /*new UpboundTypeMan[TyArr] {
   def toValSpineBounded[UpTo>: TyArr](a:TyArr):ValSpine[UpTo] = {val constrf = ConstrExt( (a: Type)=>(b:Type)=> TyArr(a,b).asInstanceOf[UpTo], new {val n="TyArr"})
                                              val awrap = Ty(a.t1)
                                              val bwrap = Ty(a.t2)
                                              Apped(Apped(constrf,awrap),bwrap)
   }
}*/
lazy val TyUnivTypeMan:TypeMan[TyUniv]= CaseClass1ToValSpineWithEnv[TyUniv,Binds[Type]](definingenv)(classOf[TyUniv])
/*new TypeMan[TyUniv] {
def toValSpine(a:TyUniv):ValSpine[TyUniv] = {val constrf = ConstrExt( (a: \\[Type])=> TyUniv(a), new {val n="TyUniv"})
                                             val awrap = Ty(a.abs)
                                             Apped(constrf,awrap)
                                           
                                     }
}*/
lazy val TyExistTypeMan:TypeMan[TyExist] = CaseClass1ToValSpineWithEnv[TyExist,Binds[Type]](definingenv)(classOf[TyExist])
/*  new TypeMan[TyExist] {
def toValSpine(a:TyExist):ValSpine[TyExist] = {val constrf = ConstrExt( (a: \\[Type])=>TyExist(a), new {val n="TyExist"})
                                              val awrap = Ty(a.abs)
                                              Apped(constrf,awrap)
                              }
}*/

}


}
 

